(declare-fun b () Bool)
(declare-fun c () Bool)
(declare-fun d () Bool)
(declare-fun j () Bool)
(declare-fun g () Bool)
(declare-fun h () Bool)
(declare-fun a () String)
(declare-fun e () String)
(declare-fun f () String)
(declare-fun i () String)
(declare-fun k () String)
(assert (= (= "-" (str.substr e 1 (str.len i))) b))
(assert (not (= b c)))
(assert (= j (= "-" i)))
(assert (= (= "" (str.substr e 1 (str.len i))) (not (= d g)) d g))
(assert (= (= "" (str.substr a (str.len f) (str.len k))) c))
(assert (= a (str.++ f k)))
(assert (= b (= b h)))
(assert (= j c h))
(assert (= e (str.++ i k)))
(check-sat)
